(set-option :opt.priority lex)
(set-option :opt.optsmt_engine farkas)
(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i11 Int)
(declare-const i13 Int)
(declare-const i14 Int)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const i15 Int)
(declare-const v12 Bool)
(push 1)
(pop 1)
(declare-const i16 Int)
(declare-const i17 Int)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const i18 Int)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const i19 Int)
(declare-const i20 Int)
(assert (or (distinct i11 i1) v1 v1))
(assert (or v9 v15 v9))
(assert (or (distinct i11 i1) v8 v8))
(assert (or (distinct i11 i1) (distinct i11 i1) (distinct i1 i14)))
(assert (or (distinct i11 i1) v8 (distinct i1 i14)))
(assert (or (distinct i1 i14) v15 v9))
(assert (or v9 v15 v1))
(assert (or v1 v15 v9))
(assert (or v9 v1 v9))
(assert (or (distinct i1 i14) v9 v9))
(assert (or (distinct i1 i14) v8 (distinct i1 i14)))
(assert (or v9 (distinct i1 i14) (distinct i11 i1)))
(assert (or v1 (distinct i1 i14) (distinct i11 i1)))
(assert (or v1 v8 (distinct i11 i1)))
(assert (or (distinct i1 i14) v1 (distinct i11 i1)))
(assert (or v8 (distinct i11 i1) (distinct i1 i14)))
(assert (or (distinct i1 i14) v9 (distinct i11 i1)))
(assert (or v15 v1 v8))
(minimize (+ i1 i2))
(maximize (- i1 i3))
(minimize (+ i1 i14))
(minimize (+ i1 i16))
(maximize (- i1 i17))
(maximize (- i1 i18))
(maximize (- i1 i19))
(minimize (+ i1 i20))
(minimize (+ i2 i4))
(minimize (+ i2 i11))
(minimize (+ i2 i16))
(maximize (- i2 i18))
(minimize (+ i3 i4))
(maximize (- i3 i11))
(maximize (- i3 i16))
(minimize (+ i3 i17))
(minimize (+ i3 i20))
(minimize (+ i4 i11))
(minimize (+ i4 i14))
(minimize (+ i4 i16))
(minimize (+ i11 i14))
(maximize (- i11 i15))
(minimize (+ i11 i16))
(minimize (+ i11 i17))
(maximize (- i11 i18))
(maximize (- i11 i19))
(minimize (+ i13 i17))
(minimize (+ i13 i19))
(maximize (- i13 i20))
(minimize (+ i14 i15))
(minimize (+ i14 i20))
(minimize (+ i15 i16))
(minimize (+ i15 i17))
(minimize (+ i15 i18))
(maximize (- i15 i19))
(minimize (+ i15 i20))
(maximize (- i16 i18))
(maximize (- i17 i19))
(minimize (+ i17 i20))
(minimize (+ i18 i19))
(maximize (- i19 i20))
(check-sat)
(exit)
